A:MsgA, k:Knd. Dec(ma-has-effect(A;k)) 

latex

Definitions	Knd, t  T, Id, x:A. B(x), x. t(x), 1of(t), map(f;as), KindDeq, deq-member(eq;x;L), b, Dec(P), a:A fp B(a), ma-has-effect(M;k), MsgA
Lemmas	msga wf, decidable assert, deq-member wf, Kind-deq wf, map wf, pi1 wf, Id wf, Knd wf